#ifndef CFGVISITOR_HPP
#define	CFGVISITOR_HPP

#include "dot.hpp"
#include "ast.hpp"
#include "cfg.hpp"
#include "monotone_framework.hpp"
#include <set>
#include <list>
#include <vector>
#include <map>
using namespace std;

class ASTnode;
class CFGvertex;
class box;
class diamond;
class CFGvisitable;
class CFGedge;


class CFGvisitor : public counter<CFGvisitor> {
public:
	CFGvisitor();
	virtual void StartVisit(CFGvertex *n) = 0;
	virtual void visit(box *n);
	virtual void visit(diamond *n);
	void visit_vertex(CFGvisitable *n);
protected:
	int runid;
};

class CFGvisitorDOT : public CFGvisitor {
public:
	CFGvisitorDOT();
	void writeDOTfile(const char *fPath);
	void StartVisit(CFGvertex *n);
	void visit(box *n);
	void visit(diamond *n);

private:
	dot	*graf;
};

class CFGvisitorFlatInfo : public CFGvisitor {
public:
	void StartVisit(CFGvertex *n);
	void visit(box *n);
	void visit(diamond *n);
	
	typedef int label_t;
	typedef pair<label_t/*source*/, label_t/*dest*/> edge;
	
	
	label_t init;
	set<label_t> final;
	list<edge> flow;
	list<edge> flowR;
	vector<CFGvertex*> labels;
	map<ASTnode*, CFGvertex*> reverse_payload;
private:
	void add_to_flows(const CFGedge& e);
	void add_to_labels(CFGvertex*);
	void handle_extremal(const CFGedge& e);
};

#endif	/* CFGVISITOR_HPP */
